;; capture avoiding beta reduction

(define (process exp)
  ;; make sure to 'process' a term before working on it
  ;; so that when we used gensym we will create fresh symbols
  ;;
  (cond ((pair? exp) (process (car exp)) (process (cdr exp)))
        ((symbol? exp) (gensym exp))
        (else #t)))

;; /!\ careful about reducing under binders /!\

(define (var? term)
  (symbol? term))

(define (app? term)
  ;; (<term> <term>)
  ;;   ^car     ^cadr
  (if (pair? term)
      (and (not (eq? 'lambda (car term)))
	   (null? (cddr term)))
      #f))

(define (lam? term)
  ;; (lambda <var> <body>)
  ;;   ^car   ^cadr   ^caddr
  (if (pair? term)
      (and (eq? 'lambda (car term))
	   (null? (cdddr term)))
      #f))

(define (lam->var term)
  (cadr term))
(define (lam->body term)
  (caddr term))

(define (substitute var body term)
  ;; change 'var' inside 'body' to 'term'
  (cond ((number? body) body)
	((var? body) (if (eq? var body)
			 term
			 body))
	((app? body) (list (substitute var (car body) term)
			   (substitute var (cadr body) term)))
	((lam? body)
	 (let ((x (lam->var body)))
	   (if (eq? x var)
	       body
	       (list 'lambda x (substitute var (lam->body body) term)))))
	(else (error 'substitute "invalid syntax" body))))

(define (redex? term)
  (and (app? term)
       (lam? (car term))))

(define (reduce-redex red)
  (let ((var (lam->var (car red)))
	(body (lam->body (car red)))
	(term (cadr red)))
    (substitute var body term)))

;; (lambda y ((lambda x (lambda y x)) y)
;;
;; would wrongly reduce to
;;
;; (lambda y (lambda y y))
;;
;; unless we rename,

(define changed? #f)

(define (beta-reduce^ term)
  (cond ((number? term) term)
	((and (app? term)
	      (eq? '1+ (car term))
	      (number? (cadr term)))
	 (set! changed? #t)
	 (+ 1 (cadr term)))
	((redex? term)
	 (set! changed? #t)
	 (reduce-redex term))
	((var? term) term)
	((app? term)
	 (let* ((x (car term))
		(y (cadr term))
		(x^ (beta-reduce^ x)))
	   (if (equal? x x^)
	       (let* ((y^ (beta-reduce^ y)))
		 (if (equal? y y^)
		     (list x y)
		     (list x y^)))
		 (list x^ y))))
	((lam? term)
	 (let* ((x (lam->var term))
                (x^ (gensym x))
                (body (lam->body term))
                (body^ (substitute x body x^)))
           (list 'lambda x^ (beta-reduce^ body^))))
	(else (error 'beta-reduce "invalid term" term))))

(define (beta-reduce term)
  (process term)
  (beta-reduce^ term))

(define (beta-reduce* trace? term)
  (when trace? (print `(reducing ,term)))
  (process term)
  (let loop ((term term))
    (set! changed? #f)
    (let ((term^ (beta-reduce^ term)))
      (if changed?
	  (begin
	    ;;       reducing
	    (when trace? (print `(-------> ,term^)))
	    (loop term^))
	  (begin
	    (when trace? (print '(done!)))
	    (when trace? (newline))
	    term^)))))



